\begin{tabbing}
$\forall$\=${\it es}$:event\_system\{i:l\}, $l$:IdLnk, ${\it tgs}$:(Id List), ${\it da}$:fpf(Knd; $k$.Type), ${\it ds}$:fpf(Id; $x$.Type),\+
\\[0ex]$f$:isect(\=(($\forall$${\it e'}$:es{-}E(${\it es}$). \+
\\[0ex]($\uparrow$es{-}isrcv(${\it es}$; ${\it e'}$))
\\[0ex]$\Rightarrow$ (es{-}lnk(${\it es}$; ${\it e'}$) = $l$)
\\[0ex]$\Rightarrow$ (es{-}tag(${\it es}$; ${\it e'}$) $\in$ ${\it tgs}$)
\\[0ex]$\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; ${\it e'}$); fpf{-}cap(${\it da}$; Kind{-}deq; es{-}kind(${\it es}$; ${\it e'}$); void)))
\\[0ex]$\wedge$ \=($\forall$$x$:Id. \+
\\[0ex]subtype\_rel(es{-}vartype(${\it es}$; source($l$); $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top))));
\-\\[0ex]$z$.(\{$e$:es{-}E(${\it es}$)$\mid$ loc($e$) = source($l$) $\in$ Id\} $\rightarrow$(\=(${\it tg}$:Id\+
\\[0ex]$\times$ fpf{-}cap(\=${\it da}$;\+
\\[0ex]Kind{-}deq;
\\[0ex]rcv($l$,${\it tg}$);
\\[0ex]void)) List))).
\-\-\-\-\\[0ex]with decls ${\it ds}$ ${\it da}$sends on $l$ from $e$ include $f$($e$) and only these for tags in ${\it tgs}$ $\in$ prop\{i:l\}
\end{tabbing}